翻訳と辞書 Words near each other ・ Q Soul Bossa Nostra ・ Q source ・ Q star ・ Q strip (magazine) ・ Q Television Network ・ Q Theatre ・ Q Train ・ Q TV ・ Q value ・ Q value (nuclear science) ・ Q wave ・ Q Who ・ Q with hook ・ Q with hook tail ・ Q with stroke ・ Q zero ・ Q&A ・ Q&A (album) ・ Q&A (Australian talk show) ・ Q&A (film) ・ Q&A (Homeland) ・ Q&A (Symantec) ・ Q&A (U.S. talk show) ・ Q&A software ・ Q&A website ・ Q'alawaña ・ Q'anjob'al ・ Q'anjobalan languages ・ Q'ara Qullu ・ Q'ara Quta (La Paz) Dictionary Lists mini英和辞書 mini和英辞書 Webster 1913 Latin-English FOLDOC Wikipedia English ウィキペディア

翻訳と辞書　辞書検索 [ 開発暫定版 ] スポンサード リンク Q zero ： ウィキペディア英語版 Q zero Q0 is Peter Andrews' formulation of the simply-typed lambda calculus, and provides a foundation for mathematics comparable to first-order logic plus set theory. It is a form of higher-order logic and closely related to the logics of the HOL theorem prover family. The theorem proving systems (TPS and ETPS ) are based on Q0. In August 2009, TPS won the first-ever competition among higher-order theorem proving systems.〔(The CADE-22 ATP System Competition (CASC-22) )〕 == Axioms of Q0 == The system has just five axioms, which can be stated as: $(1)$  $g\_T\; \backslash and\; g\_F\; =\; \backslash forall\; x\_o\; \backslash centerdot\; g\_x\_o$ $(2^\backslash alpha)$  $(=\; y\_\backslash alpha)\; \backslash supset\; \backslash centerdot\; \backslash ,\; h\_x\_\backslash alpha\; =\; h\_y\_\backslash alpha$ $(3^)$  $f\_\; =\; g\_\; =\; \backslash forall\; x\_\backslash beta\; \backslash centerdot\; f\_x\_\; =\; g\_x\_\backslash beta$ $(4)$  $(\backslash bold\; \backslash bold\_\backslash beta)\; \backslash bold\_\backslash alpha$ = \bold^_\bold_\beta $(5)$  $\backslash iota\_()\; =\; y\_i\backslash ,$ (Axioms 2, 3, and 4 are axiom schemas—families of similar axioms. Instances of Axiom 2 and Axiom 3 vary only by the types of variables and constants, but instances of Axiom 4 can have any expression replacing A and B.) The subscripted "''o''" is the type symbol for boolean values, and subscripted "''i''" is the type symbol for individual (non-boolean) values. Sequences of these represent types of functions, and can include parentheses to distinguish different function types. Subscripted Greek letters such as α and β are syntactic variables for type symbols. Bold capital letters such as , , and are syntactic variables for WFFs, and bold lower case letters such as , are syntactic variables for variables. indicates syntactic substitution at all free occurrences. The only primitive constants are , denoting equality of members of each type α, and , denoting a description operator for individuals, the unique element of a set containing exactly one individual. The symbols λ and brackets ("(and " )") are syntax of the language. All other symbols are abbreviations for terms containing these, including quantifiers ∀ and ∃. In Axiom 4, must be free for in , meaning that the substitution does not cause any occurrences of free variables of to become bound in the result of the substitution. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Q zero」の詳細全文を読む スポンサード リンク 翻訳と辞書 : 翻訳のためのインターネットリソース Copyright(C) kotoba.ne.jp 1997-2016. All Rights Reserved.